\begin{tabbing}
$\forall$\=$E$:Type$_{\mbox{\scriptsize i}}$, $T$, $V$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$), ${\it loc}$:($E$$\rightarrow$Id), ${\it kind}$:($E$$\rightarrow$Knd),\+
\\[0ex]${\it val}$:($e$:$E$$\rightarrow$eventtype(${\it kind}$;${\it loc}$;$V$;$M$;$e$)), ${\it when}$, ${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(${\it loc}$($e$),$x$)),
\\[0ex]${\it sends}$:($l$:IdLnk$\rightarrow$$E$$\rightarrow$(Msg\_sub($l$;$M$) List)), ${\it sender}$:(\{$e$:$E$$\mid$ isrcv(${\it kind}$($e$)) \}$\rightarrow$$E$),
\\[0ex]${\it index}$:($e$:\{$e$:$E$$\mid$ isrcv(${\it kind}$($e$)) \}$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$))$\parallel$}}$), ${\it first}$:($E$$\rightarrow\mathbb{B}$),
\\[0ex]${\it pred}$:(\{${\it e'}$:$E$$\mid$ $\neg$${\it first}$(${\it e'}$) \}$\rightarrow$$E$), ${\it causl}$:($E$$\rightarrow$$E$$\rightarrow$Prop$_{\mbox{\scriptsize i}}$).
\-\\[0ex]ESAxioms\=\{i:l\}\+
\\[0ex]($E$; $T$; $M$; ${\it loc}$; ${\it kind}$; ${\it val}$; ${\it when}$; ${\it after}$; ${\it sends}$; ${\it sender}$; ${\it index}$; ${\it first}$; ${\it pred}$; ${\it causl}$)
\-\\[0ex]$\in$ Prop$_{\mbox{\scriptsize i'}}$
\end{tabbing}